l:IdLnk, dt:tg:Id fp Type, knd:Knd, T:Type.
(isrcv(knd)  lnk(knd) = l  T = dt(tag(knd))?Void)  lnk-decl(l;dt) || knd : T 

latex

Definitions	Knd, x : v, f(x), lnk-decl(l;dt), P  Q, t  T, {T}, x:A. B(x), SQType(T), Prop, Top, KindDeq, P & Q, P  Q, x. t(x), a:A fp B(a), x  dom(f), b, f || g, IdLnk, Id, tag(k), IdDeq, f(x)?z, lnk(k), isrcv(k), rcv(l,tg), 1of(t), map(f;as), x:A. B(x), True, P  Q, S  T, (x  l), , b, A, S  T, False, P  Q
Lemmas	l member wf, not wf, bnot wf, bool wf, assert of bnot, eqff to assert, iff transitivity, bool sq, eqtt to assert, bool cases, member map, rcv wf, map wf, assert-deq-member, isrcv wf, lnk wf, fpf-cap wf, id-deq wf, tagof wf, fpf wf, Id wf, IdLnk wf, assert wf, fpf-dom wf, fpf-single wf, top wf, fpf-trivial-subtype-top, lnk-decl wf, fpf-single-dom, Kind-deq wf, Knd wf, Knd sq